package srcSAT;

import java.io.BufferedReader;
import java.io.BufferedWriter;
import java.io.File;
import java.io.FileInputStream;
import java.io.FileOutputStream;
import java.io.FileReader;
import java.io.FileWriter;
import java.io.IOException;
import java.io.ObjectInputStream;
import java.io.ObjectOutputStream;
import java.util.ArrayList;
import java.util.Collections;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Set;

import lib.ArgumentValidator;
import lib.logging.ANSIConsoleLogger;
import lib.logging.ILogger;

public class GraphSubsetMapper 
{
    private static List<Pair> DecodeMappingFromMinisatOutput(
            ILogger logger,
            String satMappingFile,
            String vertexCountFile,
            String minisatOutputFileName) throws IOException, ClassNotFoundException 
    {
        logger.LogInfo("Reading satVar to vertex mapping from disk");
        HashMap<Integer, Pair> satVarToVertexPairMapping = ReadSATVarsMappingFromDisk(satMappingFile);
        
        List<Integer> satisfiedSatVars = GetSatisfiedSatVarsFromMinisatOutput(minisatOutputFileName);
        logger.LogInfo("Number of satified sat vars: %d", satisfiedSatVars.size());
        
        int vertexCount = ReadVertexCount(vertexCountFile);
        return GetMappingFromSatVars(satisfiedSatVars, satVarToVertexPairMapping, logger, vertexCount);
    }
    
    private static List<Pair> GetMappingFromSatVars(
            List<Integer> satisfiedSatVars,
            HashMap<Integer, Pair> satVarToVertexPairMapping,
            ILogger logger,
            int numVertices) 
    {
        if (satisfiedSatVars.size() != numVertices)
        {
            logger.LogError(
                    "Size mismatch between number of satisfied variables (%d) " +
                        "and vertices in smaller graph (%d). " +
                        "Hence no mapping exists!",
                    satisfiedSatVars.size(),
                    numVertices);
            
            return new ArrayList<Pair>();
        }
        
        List<Pair> mapping = new ArrayList<Pair>();
        
        for (int satVar : satisfiedSatVars)
        {
            mapping.add(satVarToVertexPairMapping.get(satVar));
        }

        return mapping;
    }

    private static List<Integer> GetSatisfiedSatVarsFromMinisatOutput(String minisatOutputFileName) throws IOException 
    {
        List<Integer> satisfiedVars = new ArrayList<Integer>();
        
        BufferedReader br = new BufferedReader(new FileReader(minisatOutputFileName));
        String line = br.readLine();
        if (line.equalsIgnoreCase("SAT"))
        {
            line = br.readLine();
            line = line.trim();
            String[] splits = line.split(" ");
            for (String token : splits)
            {
                int value = Integer.parseInt(token);
                
                if (value == 0)
                {
                    break;
                }
                
                if (value > 0)
                {
                    satisfiedVars.add(value);
                }
            }
        }

        return satisfiedVars;
    }

    /**
     * @param args
     * @throws Exception 
     */
    public static void main(String[] args) throws Exception 
    {
        ILogger logger = new ANSIConsoleLogger();
        
        try
        {
            if (args.length != 2)
            {
                logger.LogError(
                        "Incorrect number of paramets: %d. " +
                        "Usage: java GraphSubsetMapper <mode: 1 (generate minisat input file) OR 2 (decode mapping from minisat output)> <test name>",
                        args.length);
    
                System.exit(1);
            }

            int runMode = Integer.parseInt(args[0]);
            String testName = args[1];
            
            String graphsFileName = testName + ".graphs";
            String minisatInputFileName = testName + ".satinput";
            String minisatOutputFileName = testName + ".satoutput";
            String mappingOutputFileName = testName + ".mapping";
            String satMappingFileName = testName + "_satMapping.data";
            String vertexCountFileName = testName + "_vertexCount.txt";
            
            if (runMode == 1)
            {
                GraphSubsetMapper graphSubsetMapper = new GraphSubsetMapper(logger, graphsFileName);
                boolean mappingPotentiallyExists = graphSubsetMapper.GenerateMinisatInputFile(
                        vertexCountFileName,
                        minisatInputFileName,
                        satMappingFileName);
                
                if (!mappingPotentiallyExists)
                {
                    WriteMappingToOutputFile(new ArrayList<Pair>(), mappingOutputFileName);
                }
            }
            else if (runMode == 2)
            {
                List<Pair> mapping = GraphSubsetMapper.DecodeMappingFromMinisatOutput(
                        logger,
                        satMappingFileName,
                        vertexCountFileName,
                        minisatOutputFileName);
                
                logger.LogInfo("mapping: %s", mapping);
                
                WriteMappingToOutputFile(mapping, mappingOutputFileName);
            }
        }
        catch (Exception ex)
        {
            logger.LogException(ex);
            throw ex;
        }
    }

    @SuppressWarnings("unchecked")
    private static HashMap<Integer, Pair> ReadSATVarsMappingFromDisk(String mappingFileName) throws IOException, ClassNotFoundException 
    {
        File mappingFile = new File(mappingFileName);
        
        if (!mappingFile.exists())
        {
            throw new IOException(
                    "Unabe to read SAT vars mapping as file " + 
                        mappingFile.getAbsolutePath() + "does not exist!");
        }
        
        FileInputStream fin = new FileInputStream(mappingFile);
        ObjectInputStream ois = new ObjectInputStream(fin);
        HashMap<Integer, Pair> mapping = (HashMap<Integer, Pair>) ois.readObject();
        ois.close();
        
        return mapping;
    }

    private static int ReadVertexCount(String vertexCountFileName) throws NumberFormatException, IOException 
    {
        BufferedReader br = new BufferedReader(new FileReader(vertexCountFileName));
        int vertexCount = Integer.parseInt(br.readLine());
        br.close();
        
        return vertexCount; 
    }
    
    private static void WriteMappingToOutputFile(List<Pair> mapping, String outputFile) throws IOException 
    {
        BufferedWriter bufWriter = new BufferedWriter(
                new FileWriter(outputFile, false));
        
        if (mapping.size() == 0)
        {
            bufWriter.write("0");
            bufWriter.close();
            return;
        }
        
        for (int i = 0; i < mapping.size(); ++i)
        {
            Pair pair = mapping.get(i);
            StringBuilder sb = new StringBuilder();
            sb.append(pair.X());
            sb.append(" ");
            sb.append(pair.Y());
            
            bufWriter.write(sb.toString());
            
            if (i != (mapping.size() -1))
            {
                bufWriter.newLine();
            }
        }
        
        bufWriter.close();
    }
    private static void WriteVertexCountFile(String fileName, int vertexCount) throws IOException 
    {
        BufferedWriter bw = new BufferedWriter(new FileWriter(fileName));
        bw.write(Integer.toString(vertexCount));
        bw.close();
    }
    private Graph smallerGraph;
    private Graph largerGraph;
    
    private HashMap<Integer, List<Integer>> notNeighborMapForSmallerGraph;

    private ILogger logger;

    public GraphSubsetMapper(ILogger logger, String graphsFileName) throws IOException
    {
        ArgumentValidator.IsNotNull("logger", logger);
        ArgumentValidator.IsNotNullOrEmpty("graphsFileName", graphsFileName);
        
        this.logger = logger;
        InitializeGraphsFromInputFile(graphsFileName);
    }

    private boolean ContainsAny(
            List<Integer> nborPotentialCandidates,
            List<Integer> eligibleCandidates) 
    {
        for (int eligibleCandidate : eligibleCandidates)
        {
            if (nborPotentialCandidates.contains(eligibleCandidate))
            {
                return true;
            }
        }
        
        return false;
    }

    private boolean DoesEachVertexHavePotentialCandidates(HashMap<Integer, List<Integer>> potentialCandidatesMap) 
    {
        int singletons = 0;
        for (int smallVertex : potentialCandidatesMap.keySet())
        {
            if (potentialCandidatesMap.get(smallVertex).isEmpty())
            {
                logger.LogError("No potential candidates for small graph vertex: %d", smallVertex);
                return false;
            }
            else if (potentialCandidatesMap.get(smallVertex).size() == 1)
            {
                ++singletons;
                logger.LogInfo("Found singleton! %d: %s", smallVertex, potentialCandidatesMap.get(smallVertex));
            }
        }
        
        logger.LogInfo("Total singletons: %d", singletons);
        return true;
    }

    private boolean GenerateMinisatInputFile(
            String vertexCountFileName,
            String minisatInputFileName,
            String satVarMappingFileName) throws IOException 
    {
        HashMap<Integer, List<Integer>> potentialCandidatesMap = GetPotentialCandidatesMap();
        PruneCandidatesBasedOnNbors(potentialCandidatesMap);
        
        // Devnote (Abhip): 
        // Pruning based on non neighbors is computationally expensive, 
        // as a vertex generally has many non-neighbors, and the pruning algo goes thru each one of them.
        // Also, it didn't give much benefit over the neighbor based pruning. Hence skipping pruning on non-neighbors.
        // 
        // PruneCandidatesBasedOnNonNbors(potentialCandidatesMap);
        
        if (!DoesEachVertexHavePotentialCandidates(potentialCandidatesMap))
        {
            logger.LogError(
                    "One or more small graph vertices have no potential candidates in larger graph. Hence no mapping exists!");
            
            return false;
        }
        
        HashMap<Pair, Integer> vertexPairToSATVarMapping = GetVertexPairToSATVarMapping(potentialCandidatesMap);
        
        HashMap<Integer, Pair> satVarToVertexPairMapping = GetSatVarToVertexPairMapping(vertexPairToSATVarMapping);
        
        Set<Integer> allSATVars = satVarToVertexPairMapping.keySet();
        
        logger.LogInfo(
                "Smaller graph: nodes: %d, edges: %d, density: %f",
                this.smallerGraph.Vertices().size(),
                this.smallerGraph.Edges().size(),
                this.smallerGraph.Density());
        
        logger.LogInfo(
                "Larger graph: nodes: %d, edges: %d, density: %f",
                this.largerGraph.Vertices().size(),
                this.largerGraph.Edges().size(),
                this.largerGraph.Density());
        
        logger.LogInfo("Number of sat vars: %d", allSATVars.size());
        
        HashMap<Integer, List<Integer>> smallerGraphVerticesToSATVarMapping = GetSmallerGraphVerticesToSATVarMapping(
                potentialCandidatesMap,
                vertexPairToSATVarMapping);

        logger.LogInfo("Generating: %s", "eachVarHasAtleastOneValueClauses");
        List<Clause> eachVarHasAtleastOneValueClauses = GetEachVarHasAtleastOneValueClauses(smallerGraphVerticesToSATVarMapping);
        
        logger.LogInfo("Generating: %s", "noVarHasTwoValuesClauses");
        List<Clause> noVarHasTwoValuesClauses = GetNoVarHasTwoValuesClauses(smallerGraphVerticesToSATVarMapping);

        logger.LogInfo("Generating: %s", "noTwoVerticesMapToSameVertexClauses");
        List<Clause> noTwoVerticesMapToSameVertexClauses = GetNoTwoVerticesMapToSameVertexClauses(vertexPairToSATVarMapping);

        logger.LogInfo("Generating: %s", "edgeConstraintsClauses");
        List<Clause> edgeConstraintsClauses = GetEdgeConstrainsClauses(
                allSATVars,
                vertexPairToSATVarMapping,
                satVarToVertexPairMapping);
        
        logger.LogInfo("Generating: %s", "allClauses");
        List<Clause> allClauses = new ArrayList<Clause>(eachVarHasAtleastOneValueClauses);
        allClauses.addAll(noVarHasTwoValuesClauses);
        allClauses.addAll(noTwoVerticesMapToSameVertexClauses);
        allClauses.addAll(edgeConstraintsClauses);

        logger.LogInfo("Number of clauses: %d", allClauses.size());
        
        logger.LogInfo("writing sat input file.");
        WriteMinisatInputFile(allSATVars.size(), allClauses, minisatInputFileName);
        
        logger.LogInfo("Saving satVar to vertex mapping to disk");
        WriteSATVarsMappingToDisk(satVarToVertexPairMapping, satVarMappingFileName);
        
        logger.LogInfo("Saving vertex count %d to %s", smallerGraph.Vertices().size(), vertexCountFileName);
        WriteVertexCountFile(
                vertexCountFileName,
                smallerGraph.Vertices().size());
        
        /*
        logger.LogInfo("vertexPairToSATVariableMapping:%s", vertexPairToSATVarMapping);
        logger.LogInfo("satVariableToVertexPairMapping:%s", satVarToVertexPairMapping);
        logger.LogInfo("smallerGraphVerticesToSATVariableMapping:%s", smallerGraphVerticesToSATVarMapping);
        logger.LogInfo("notNeighborMapForSmallerGraph:%s", notNeighborMapForSmallerGraph);
        
        logger.LogInfo("eachVarHasAtleastOneValueClauses: count:%d, %s", eachVarHasAtleastOneValueClauses.size(), eachVarHasAtleastOneValueClauses);
        logger.LogInfo("noVarHasTwoValuesClauses: count:%d, %s", noVarHasTwoValuesClauses.size(),noVarHasTwoValuesClauses);
        logger.LogInfo("noTwoVerticesMapToSameVertexClauses: count:%d, %s", noTwoVerticesMapToSameVertexClauses.size(), noTwoVerticesMapToSameVertexClauses);
        logger.LogInfo("edgeConstraintsClauses: count:%d, %s", edgeConstraintsClauses.size(), edgeConstraintsClauses);
        logger.LogInfo("allClauses: count:%d, %s", allClauses.size(), allClauses);
        */
        
        return true;
    }

    private List<Clause> GetEachVarHasAtleastOneValueClauses(
            HashMap<Integer, List<Integer>> smallerGraphVerticesToSATVarMapping) 
    {
        // For eg, vertex 1 in smaller graph maps to some vertex in larger graph
        // i.e, X11 v X12 v X13 ...
        
        List<Clause> clauses = new ArrayList<Clause>();
        for (int smallerGraphVertex : smallerGraphVerticesToSATVarMapping.keySet())
        {
            if (!smallerGraphVerticesToSATVarMapping.get(smallerGraphVertex).isEmpty())
            {
                clauses.add(new Clause(smallerGraphVerticesToSATVarMapping.get(smallerGraphVertex)));
            }
            
        }
        
        return clauses;
    }

    private List<Clause> GetEdgeConstrainsClauses(
            Set<Integer> allSATVars,
            HashMap<Pair, Integer> vertexPairToSATVarMapping,
            HashMap<Integer, Pair> satVarToVertexPairMapping) 
    {
        // Basic idea: if vertex A from small graph maps to vertex P in larger graph,
        // then, all neighbors of A must map to some neighbor of P
        // and, all vertices not neighbor to A, must not map to any neighbor of P
        // For eg, small graph has 1 -> 2,3
        // large graph has 1 -> 4,5
        // then, X11 -> (X24 v X25) ^ (X34 v X35)
        // in CNF: (~X11 v X24 v X25) ^ (~X11 v X34 v X35)
        
        
        List<Clause> clauses = new ArrayList<Clause>();
        for (int satVar : allSATVars)
        {
            Pair pair = satVarToVertexPairMapping.get(satVar);
            
            List<Integer> nborsOfSmallGraphVertex = this.smallerGraph.Neighbors(pair.X());
            List<Integer> nborsOfLargerGraphVertex = this.largerGraph.Neighbors(pair.Y());
            
            for (int smallGraphVertexNbor : nborsOfSmallGraphVertex)
            {
                List<Integer> clauseVars = new ArrayList<Integer>();
                clauseVars.add(-1 * satVar);
                
                boolean anyClauseVarAdded = false;
                for (int largerGraphVertexNbor : nborsOfLargerGraphVertex)
                {
                    Pair p = new Pair(smallGraphVertexNbor, largerGraphVertexNbor);
                    if (vertexPairToSATVarMapping.containsKey(p))
                    {
                        anyClauseVarAdded = true;
                        clauseVars.add(vertexPairToSATVarMapping.get(p));
                    }
                }

                if (!anyClauseVarAdded)
                {
                    continue;
                }
                
                clauses.add(new Clause(clauseVars));
            }
            
            List<Integer> nonNborsOfSmallGraphVertex = notNeighborMapForSmallerGraph.get(pair.X());
            for (int nonNeighbor : nonNborsOfSmallGraphVertex)
            {
                for (int largerGraphVertexNbor : nborsOfLargerGraphVertex)
                {
                    List<Integer> clauseVars = new ArrayList<Integer>();
                    clauseVars.add(-1 * satVar);
                    
                    Pair p = new Pair(nonNeighbor, largerGraphVertexNbor);
                    if (vertexPairToSATVarMapping.containsKey(p))
                    {
                        clauseVars.add(-1 * vertexPairToSATVarMapping.get(p));
                        clauses.add(new Clause(clauseVars));
                    }
                }
            }
        }

        return clauses;
    }

    private HashMap<Integer, List<Integer>> GetNotNeighborMapForSmallerGraph() 
    {
        HashMap<Integer, List<Integer>> map = new HashMap<Integer, List<Integer>>();
        
        for (int vertex : this.smallerGraph.Vertices())
        {
            List<Integer> vertices = new ArrayList<Integer>(this.smallerGraph.Vertices());
            List<Integer> nbors = new ArrayList<Integer>(this.smallerGraph.Neighbors(vertex));
            vertices.removeAll(nbors);
            vertices.remove(new Integer(vertex));
            map.put(vertex, vertices);
        }

        return map;
    }

    private List<Clause> GetNoTwoVerticesMapToSameVertexClauses(
            HashMap<Pair, Integer> vertexPairToSATVarMapping) 
    {
        
        // Any two vertices of smaller graph, should not map to same vertex in larger graph 
        // ~(X11 ^ X21) ^ ~(X21 ^ X31) ^ ...
        // CNF clauses: ~X11 v ~X21;  ~X21 v ~X31; ...
        
        List<Clause> clauses = new ArrayList<Clause>();
        for (int largeGraphVertex : this.largerGraph.Vertices())
        {
            List<Integer> satVars = new ArrayList<Integer>();
            for (int smallGraphVertex : this.smallerGraph.Vertices())
            {
                Pair pair = new Pair(smallGraphVertex, largeGraphVertex);
                if (vertexPairToSATVarMapping.containsKey(pair))
                {
                    satVars.add(vertexPairToSATVarMapping.get(pair));
                }
            }
            
            // we got satVars which map various small graph vertices to 'largeGraphVertex'
            // generate clauses saying any two such satVars cannot be true at the same time
            
            for (int i = 0; i < satVars.size(); ++i)
            {
                for (int j = i+1; j < satVars.size(); ++j)
                {
                    List<Integer> clauseVars = new ArrayList<Integer>();
                    clauseVars.add(-1 * satVars.get(i));
                    clauseVars.add(-1 * satVars.get(j));
                    
                    clauses.add(new Clause(clauseVars));
                }
            }
            
        }
        
        return clauses;
    }

    private List<Clause> GetNoVarHasTwoValuesClauses(
            HashMap<Integer, List<Integer>> smallerGraphVerticesToSATVarMapping) 
    {
        // For eg, any two vars corresponding to vertex 1 in smaller graph, should not be true at same time
        // i.e, ~(X11 ^ X12) ^ ~(X11 ^ X13) ...
        // CNF clauses: ~X11 v ~X12; ~X11 v ~X13; ...
        
        List<Clause> clauses = new ArrayList<Clause>();
        for (int smallerGraphVertex : smallerGraphVerticesToSATVarMapping.keySet())
        {
            List<Integer> satVars = smallerGraphVerticesToSATVarMapping.get(smallerGraphVertex);
            
            for (int i = 0; i < satVars.size(); ++i)
            {
                for (int j = i+1; j < satVars.size(); ++j)
                {
                    List<Integer> clauseVars = new ArrayList<Integer>();
                    clauseVars.add(-1 * satVars.get(i));
                    clauseVars.add(-1 * satVars.get(j));
                    
                    clauses.add(new Clause(clauseVars));
                }
            }
        }
        
        return clauses;
    }

    private HashMap<Integer, List<Integer>> GetPotentialCandidatesMap() 
    {
        HashMap<Integer, List<Integer>> potentialCandidatesMap = new HashMap<Integer, List<Integer>>();
        
        List<Integer> smallerGraphVertices = this.smallerGraph.Vertices();
        List<Integer> largerGraphVertices = this.largerGraph.Vertices();
        
        for (int smallerGraphVertex : smallerGraphVertices)
        {
            List<Integer> potentialCandidates = new ArrayList<Integer>();
            
            for (int largerGraphVertex: largerGraphVertices)
            {
                if (largerGraph.Degree(largerGraphVertex) >= smallerGraph.Degree(smallerGraphVertex))
                {
                    potentialCandidates.add(largerGraphVertex);
                }
            }
            
            Collections.sort(potentialCandidates);
            potentialCandidatesMap.put(smallerGraphVertex, potentialCandidates);
        }

        return potentialCandidatesMap;
    }

    private HashMap<Integer, Pair> GetSatVarToVertexPairMapping(
            HashMap<Pair, Integer> vertexPairToSATVariableMapping) 
    {
        HashMap<Integer, Pair> mapping = new HashMap<Integer, Pair>();
        
        for (Pair key : vertexPairToSATVariableMapping.keySet())
        {
            mapping.put(vertexPairToSATVariableMapping.get(key), key);
        }
        
        return mapping;
    }

    private HashMap<Integer, List<Integer>> GetSmallerGraphVerticesToSATVarMapping(
            HashMap<Integer, List<Integer>> potentialCandidatesMap,
            HashMap<Pair, Integer> vertexPairToSATVariableMapping) 
    {
        HashMap<Integer, List<Integer>> mapping = new HashMap<Integer, List<Integer>>();
        
        for (int smallGraphVertex : potentialCandidatesMap.keySet())
        {
            List<Integer> satVars = new ArrayList<Integer>();
            
            for (int candidate : potentialCandidatesMap.get(smallGraphVertex))
            {
                satVars.add(vertexPairToSATVariableMapping.get(new Pair(smallGraphVertex, candidate)));
            }
            
            mapping.put(smallGraphVertex, satVars);
        }
        
        return mapping;
    }

    private HashMap<Pair, Integer> GetVertexPairToSATVarMapping(
            HashMap<Integer, List<Integer>> potentialCandidatesMap) 
    {
        HashMap<Pair, Integer> mapping = new HashMap<Pair, Integer>();
        
        int satVariableNumber = 0;
        
        for (int key : potentialCandidatesMap.keySet())
        {
            List<Integer> candidates = potentialCandidatesMap.get(key);
            for (int candidate: candidates)
            {
                mapping.put(new Pair(key, candidate), ++satVariableNumber);
            }
            
        }
        return mapping;
    }

    private void InitializeGraphsFromInputFile(String graphsFileName) throws IOException 
    {
        // using HashSet at input might have duplicates
        HashSet<Edge> edges1 = new HashSet<Edge>();
        HashSet<Edge> edges2 = new HashSet<Edge>();
        
        boolean readingFirstGraph = true;
        
        BufferedReader br = new BufferedReader(new FileReader(graphsFileName));
        String line = null;
        while ((line = br.readLine()) != null)
        {
            line = line.trim();
            String[] splits = line.split(" ");
            int value1 = Integer.parseInt(splits[0]);
            int value2 = Integer.parseInt(splits[1]);
            
            if ((value1 == 0) && value2 == 0)
            {
                readingFirstGraph = false;
                continue;
            }
            
            if (readingFirstGraph)
            {
                edges1.add(new Edge(value1, value2));
            }
            else
            {
                edges2.add(new Edge(value1, value2));
            }
        }
        
        this.largerGraph = new Graph(new ArrayList<Edge>(edges1));
        this.smallerGraph = new Graph(new ArrayList<Edge>(edges2));
        this.notNeighborMapForSmallerGraph = GetNotNeighborMapForSmallerGraph();
    }

    private void PruneCandidatesBasedOnNbors(HashMap<Integer, List<Integer>> potentialCandidatesMap) 
    {
        for (int smallGraphVertex : smallerGraph.Vertices())
        {
            List<Integer> potentialCandidates = new ArrayList<Integer>(potentialCandidatesMap.get(smallGraphVertex));
            
            for (int potentialCandidate : potentialCandidates)
            {
                List<Integer> candidatesToPrune = new ArrayList<Integer>();
                List<Integer> eligibleCandidates = largerGraph.Neighbors(potentialCandidate);
                
                for (int nbor : smallerGraph.Neighbors(smallGraphVertex))
                {
                    if(!ContainsAny(potentialCandidatesMap.get(nbor), eligibleCandidates))
                    {
                        candidatesToPrune.add(potentialCandidate);
                        break;
                    }
                }
                
                if (candidatesToPrune.size() > 0)
                {
                    potentialCandidatesMap.get(smallGraphVertex).removeAll(candidatesToPrune);
                }
            }
        }
    }

    /*
    private void PruneCandidatesBasedOnNonNbors(HashMap<Integer, List<Integer>> potentialCandidatesMap) 
    {
        for (int smallGraphVertex : smallerGraph.Vertices())
        {
            List<Integer> potentialCandidates = new ArrayList<Integer>(potentialCandidatesMap.get(smallGraphVertex));
            
            for (int potentialCandidate : potentialCandidates)
            {
                List<Integer> candidatesToPrune = new ArrayList<Integer>();
                List<Integer> potentialCandidateNbors = largerGraph.Neighbors(potentialCandidate);
                
                List<Integer> invalidCandidates = new ArrayList<Integer>(potentialCandidateNbors);
                invalidCandidates.add(potentialCandidate);
                
                for (int nonNbor : notNeighborMapForSmallerGraph.get(smallGraphVertex))
                {
                    List<Integer> nonNborPotentialCandidates = new ArrayList<Integer>(potentialCandidatesMap.get(nonNbor));
                    nonNborPotentialCandidates.removeAll(invalidCandidates);
                    
                    if (nonNborPotentialCandidates.isEmpty())
                    {
                        candidatesToPrune.add(potentialCandidate);
                        break;
                    }
                }
                
                if (candidatesToPrune.size() > 0)
                {
                    potentialCandidatesMap.get(smallGraphVertex).removeAll(candidatesToPrune);
                }
            }
        }
    }
    */

    private void WriteMinisatInputFile(
            int numberOfSatVars,
            List<Clause> allClauses,
            String minisatInputFileName) throws IOException 
    {
        BufferedWriter bufWriter = new BufferedWriter(
                new FileWriter(minisatInputFileName, false));
        
        String data;
        data = "c Clauses for GraphSubsetMapping problem";
        bufWriter.write(data);
        bufWriter.newLine();
        
        data = "p cnf " + numberOfSatVars + " " + allClauses.size();
        bufWriter.write(data);
        bufWriter.newLine();
        
        for (Clause clause : allClauses)
        {
            StringBuilder sb = new StringBuilder();
            for (int clauseVar : clause.Variables())
            {
                sb.append(clauseVar);
                sb.append(" ");
            }
            
            sb.append(0);
            
            bufWriter.write(sb.toString());
            bufWriter.newLine();
        }
        
        bufWriter.close();
    }

    private void WriteSATVarsMappingToDisk(
            HashMap<Integer, Pair> satVarToVertexPairMapping,
            String satVarMappingFileName) throws IOException 
    {
        File satVarMappingFile = new File(satVarMappingFileName);
        if (satVarMappingFile.exists())
        {
            satVarMappingFile.delete();
        }
        
        FileOutputStream fout = new FileOutputStream(satVarMappingFile);
        ObjectOutputStream oos = new ObjectOutputStream(fout);
        oos.writeObject(satVarToVertexPairMapping);
        oos.close();
    }
}
